package bcontractor.partialmeet.operators;

import java.util.Collections;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.Queue;
import java.util.Set;

import bcontractor.api.SATReasoner;
import bcontractor.api.Sentence;
import bcontractor.api.SentenceSet;
import bcontractor.base.SetUtils;
import bcontractor.partialmeet.RemainderSet;
import bcontractor.partialmeet.RemainderSetOperator;

/**
 * An implementation of the remainder set operator loosely based on the ideas of the correspondent kernel operator.
 * 
 * @author lundberg
 * 
 */
public class BlackboxRemainderSetOperator<S extends Sentence<S>> implements RemainderSetOperator<S> {

	private final SATReasoner<S> reasoner;

	/**
	 * Constructor
	 * 
	 * @param reasoner reasoner
	 */
	public BlackboxRemainderSetOperator(SATReasoner<S> reasoner) {
		this.reasoner = reasoner;
	}

	/**
	 * {@inheritDoc}
	 */
	@Override
	public RemainderSet<S> eval(SentenceSet<S> base, S sentence) {
		return new RemainderSet<S>(this.findElements(base, sentence));
	}

	/**
	 * 
	 * @param base base
	 * @param sentence sentence
	 * @return set of all remainder sets
	 */
	private Set<SentenceSet<S>> findElements(SentenceSet<S> base, S sentence) {
		if (!this.reasoner.entails(base, sentence)) {
			return Collections.singleton(base);
		}
		Set<SentenceSet<S>> cut = new HashSet<SentenceSet<S>>();
		Set<SentenceSet<S>> remainderSet = new HashSet<SentenceSet<S>>();
		Queue<SentenceSet<S>> queue = new LinkedList<SentenceSet<S>>();
		queue.add(SetUtils.<S> emptySentenceSet());

		while (!queue.isEmpty()) {
			SentenceSet<S> hn = queue.remove();
			if (!this.cutContainsSet(cut, hn)) {
				SentenceSet<S> r = this.blackbox(hn, base, sentence);
				if (r == null) {
					cut.add(hn);
				} else {
					remainderSet.add(r);
					for (S b : base.without(r)) {
						queue.add(hn.with(b));
					}
				}
			}
		}
		return remainderSet;
	}

	/**
	 * Verifies if the cut already contains the set, meaning searching upon it would be useless.
	 * 
	 * @param cut cut
	 * @param hn hn
	 * @return boolean
	 */
	private boolean cutContainsSet(Set<SentenceSet<S>> cut, SentenceSet<S> hn) {
		for (SentenceSet<S> c : cut) {
			if (hn.containsAll(c)) {
				return true;
			}
		}
		return false;
	}

	/**
	 * Finds a maximal subset of the given base that fails to entail the sentence
	 * 
	 * @param base base
	 * @param sentence sentence
	 * @return subset of sentenses that entail the sentence
	 */
	private SentenceSet<S> blackbox(SentenceSet<S> hn, SentenceSet<S> base, S sentence) {
		return this.expand(this.shrink(hn, base, sentence), hn, base, sentence);
	}

	/**
	 * Finds a subset of the base that fails to entail the given sentence , excluding elements not found on hn
	 * 
	 * @param hn hn
	 * @param base base
	 * @param sentence sentence
	 * @return subset that does not entail the sentence
	 */
	private SentenceSet<S> shrink(SentenceSet<S> hn, SentenceSet<S> base, S sentence) {
		SentenceSet<S> subset = base;
		for (S b : base.without(hn)) {
			subset = subset.without(b);
			if (!this.reasoner.entails(subset, sentence)) {
				return subset;
			}
		}
		return null;
	}

	/**
	 * Given a subset of the base that fails to entail the sentence, finds a maximal subset of the base that still fails
	 * to entail the sentence.
	 * 
	 * @param subset subset
	 * @param base base
	 * @param sentence sentence
	 * @return a maximal subset of base that does not entail the sentence
	 */
	private SentenceSet<S> expand(SentenceSet<S> subset, SentenceSet<S> hn, SentenceSet<S> base, S sentence) {
		if (subset == null) {
			return null;
		}
		for (S b : base.without(subset).without(hn)) {
			if (!this.reasoner.entails(subset.with(b), sentence)) {
				subset = subset.with(b);
			}
		}
		return subset.isEmpty() ? null : subset;
	}
}
